| Definitions | Raframe-k(x1), P   Q, t  T, Rbframe-k(x1), ( x,yL.P(x;y)), DeclaredType(ds;x), tl(l), {i..j }, R-Feasible(R),   b, Rsends-ds(x1), f(x), x : v, {T}, Rsends?(x1), True, Rbframe-L(x1), Rsends-g(x1), Rpre?(x1), p  q, Rsends-dt(x1), Rplus-left(x1), R-interface-compat(A;B), A & B, Reffect?(x1), Reffect-x(x1), Rsframe?(x1), SQType(T), Reffect-ds(x1), Rrframe-L(x1), false, P & Q, i j, Rsends-l(x1), isrcv(k), i<j, 2of(t), nth_tl(n;as), Rda(R),  x:A. B(x), Rsframe-tag(x1), Rframe-x(x1), Rplus-right(x1), Rrframe?(x1), i j < k, if b t else f fi, Reffect-knd(x1), true, Rsends-T(x1), Id, Raframe?(x1), R-base-domain(R), l[i], i=j, xL. P(x), x:A. B(x), hd(l), Rsframe-L(x1), Rbframe?(x1), AB, Rpre-a(x1), Rrframe-x(x1), Top, Reffect-T(x1), A || B,  x. t(x), map(f;as),  b, 1of(t), Rframe?(x1), Y, A, Rds(R), False, R-frame-compat(A;B), Rsframe-lnk(x1), R-loc(R), Raframe-L(x1), "$x", Prop, ||as||, Rsends-knd(x1), at src(l):action $a(m) precondition P sends [$tg,f] on link l, isl(x), p = q, Rpre-ds(x1), locl(a), Rplus?(x1), Rframe-L(x1), Rnone?(x1), IdLnk, Dec(P), (x l), x(s),  , Unit,  , P  Q, P  Q,  |
Type, P:(State(ds)
